$\forall$${\it es}$:ES, $X$:AbsInterface(Top), $e$:E.
\\[0ex]($\uparrow$($e$ $\in_{b}$ prior($X$)))
\\[0ex]$\Rightarrow$ (prior($X$)($e$) = if pred($e$) $\in_{b}$ $X$ then pred($e$) else prior($X$)(pred($e$)) fi  $\in$ E)